{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": 1,
   "id": "certain-designation",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "1\n",
      "2\n",
      "3\n",
      "4\n",
      "5\n",
      "6\n",
      "7\n",
      "8\n",
      "9\n",
      "10\n",
      "11\n",
      "12\n",
      "13\n",
      "14\n",
      "15\n",
      "16\n",
      "17\n",
      "18\n",
      "19\n",
      "20\n",
      "21\n",
      "22\n",
      "23\n",
      "24\n",
      "25\n",
      "26\n",
      "27\n",
      "28\n",
      "29\n",
      "30\n",
      "31\n",
      "32\n",
      "33\n",
      "34\n",
      "35\n",
      "36\n",
      "stack:  782448\n"
     ]
    }
   ],
   "source": [
    "import sys\n",
    "sys.path.append(\"../\")\n",
    "from utils import *\n",
    "from instructions import Instruction\n",
    "from settings import *\n",
    "from uncompute import *\n",
    "\n",
    "n = 36\n",
    "input_file = \"../32symbolic_nomem/return-from-loop-1-35.btor2\"\n",
    "current_settings = get_btor2_settings(input_file)\n",
    "Instruction.all_instructions = read_file(input_file, modify_memory_sort=True, setting=current_settings)\n",
    "Instruction.with_grover = 0\n",
    "\n",
    "for i in range(1, n+1):\n",
    "    print(i)\n",
    "    Instruction.current_n = i\n",
    "    for instruction in Instruction.all_instructions.values():\n",
    "        if instruction[1] == INIT and i == 1:\n",
    "            Instruction(instruction).execute()\n",
    "        elif instruction[1] == NEXT or instruction[1] == BAD:\n",
    "            Instruction(instruction).execute()\n",
    "\n",
    "result_bad_states = Instruction.or_bad_states()\n",
    "assert(len(result_bad_states) == 1)\n",
    "\n",
    "print(\"stack: \", Instruction.global_stack.size)\n"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "id": "surprised-reading",
   "metadata": {},
   "outputs": [],
   "source": [
    "circuit_queue = get_circuit_queue(Instruction.global_stack)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "id": "stunning-spray",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "78580 782448\n"
     ]
    }
   ],
   "source": [
    "print(Instruction.circuit.width(), circuit_queue.size)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "id": "returning-fruit",
   "metadata": {},
   "outputs": [],
   "source": [
    "def are_all_controls_true(values, controls):\n",
    "    for c in controls:\n",
    "        if values[c] == 0:\n",
    "            return False\n",
    "        else:\n",
    "            assert(values[c] == 1)\n",
    "    return True\n",
    "\n",
    "def check_input(value):\n",
    "    # we only set the value of the first input the other ones are set to |0>\n",
    "    qubit_values = {}\n",
    "    for qword in Instruction.input_nids:\n",
    "        for i in range(n+1):\n",
    "            if i in qword.states.keys():\n",
    "                temp_value = value\n",
    "                for qubit in qword.states[i][0]:\n",
    "                    qubit_values[qubit] = temp_value % 2\n",
    "                    temp_value = temp_value // 2\n",
    "    element: Element = circuit_queue.pop()\n",
    "    assert(element.element_type != CHECKPOINT_TYPE)\n",
    "    while element.element_type != CHECKPOINT_TYPE:\n",
    "        for o in element.operands:\n",
    "            if o not in qubit_values.keys():\n",
    "                qubit_values[o] = 0\n",
    "\n",
    "        assert (element.target is not None)\n",
    "\n",
    "        if element.target not in qubit_values.keys():\n",
    "            qubit_values[element.target] = 0\n",
    "\n",
    "        flip_target = True\n",
    "        if element.gate_name == X:\n",
    "            assert(len(element.operands) == 0)\n",
    "\n",
    "        else:\n",
    "            assert((element.gate_name == CX and len(element.operands) ==1) or\n",
    "                   (element.gate_name == CCX and len(element.operands) == 2) or\n",
    "                    element.gate_name == MCX)\n",
    "            flip_target = are_all_controls_true(qubit_values, element.operands)\n",
    "\n",
    "        if flip_target:\n",
    "            qubit_values[element.target] = (qubit_values[element.target] + 1) % 2\n",
    "        circuit_queue.push(element)\n",
    "        element = circuit_queue.pop()\n",
    "    assert element.element_type == CHECKPOINT_TYPE\n",
    "    circuit_queue.push(element)\n",
    "    lines = []\n",
    "    for (bad_state, line) in Instruction.bad_states_to_line_no.items():\n",
    "        if qubit_values[bad_state] == 1:\n",
    "            lines.append(line)\n",
    "    return qubit_values[result_bad_states[0]], lines"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "id": "current-exclusive",
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "0 (0, [])\n",
      "1 (0, [])\n",
      "2 (0, [])\n",
      "3 (0, [])\n",
      "4 (0, [])\n",
      "5 (0, [])\n",
      "6 (0, [])\n",
      "7 (0, [])\n",
      "8 (0, [])\n",
      "9 (0, [])\n",
      "10 (0, [])\n",
      "11 (0, [])\n",
      "12 (0, [])\n",
      "13 (0, [])\n",
      "14 (0, [])\n",
      "15 (0, [])\n",
      "16 (0, [])\n",
      "17 (0, [])\n",
      "18 (0, [])\n",
      "19 (0, [])\n",
      "20 (0, [])\n",
      "21 (0, [])\n",
      "22 (0, [])\n",
      "23 (0, [])\n",
      "24 (0, [])\n",
      "25 (0, [])\n",
      "26 (0, [])\n",
      "27 (0, [])\n",
      "28 (0, [])\n",
      "29 (0, [])\n",
      "30 (0, [])\n",
      "31 (0, [])\n",
      "32 (0, [])\n",
      "33 (0, [])\n",
      "34 (0, [])\n",
      "35 (0, [])\n",
      "36 (0, [])\n",
      "37 (0, [])\n",
      "38 (0, [])\n",
      "39 (0, [])\n",
      "40 (0, [])\n",
      "41 (0, [])\n",
      "42 (0, [])\n",
      "43 (0, [])\n",
      "44 (0, [])\n",
      "45 (0, [])\n",
      "46 (0, [])\n",
      "47 (0, [])\n",
      "48 (1, [80000013])\n",
      "49 (0, [])\n",
      "50 (0, [])\n",
      "51 (0, [])\n",
      "52 (0, [])\n",
      "53 (0, [])\n",
      "54 (0, [])\n",
      "55 (0, [])\n",
      "56 (0, [])\n",
      "57 (0, [])\n",
      "58 (0, [])\n",
      "59 (0, [])\n",
      "60 (0, [])\n",
      "61 (0, [])\n",
      "62 (0, [])\n",
      "63 (0, [])\n",
      "64 (0, [])\n",
      "65 (0, [])\n",
      "66 (0, [])\n",
      "67 (0, [])\n",
      "68 (0, [])\n",
      "69 (0, [])\n",
      "70 (0, [])\n",
      "71 (0, [])\n",
      "72 (0, [])\n",
      "73 (0, [])\n",
      "74 (0, [])\n",
      "75 (0, [])\n",
      "76 (0, [])\n",
      "77 (0, [])\n",
      "78 (0, [])\n",
      "79 (0, [])\n",
      "80 (0, [])\n",
      "81 (0, [])\n",
      "82 (0, [])\n",
      "83 (0, [])\n",
      "84 (0, [])\n",
      "85 (0, [])\n",
      "86 (0, [])\n",
      "87 (0, [])\n",
      "88 (0, [])\n",
      "89 (0, [])\n",
      "90 (0, [])\n",
      "91 (0, [])\n",
      "92 (0, [])\n",
      "93 (0, [])\n",
      "94 (0, [])\n",
      "95 (0, [])\n",
      "96 (0, [])\n",
      "97 (0, [])\n",
      "98 (0, [])\n",
      "99 (0, [])\n",
      "100 (0, [])\n",
      "101 (0, [])\n",
      "102 (0, [])\n",
      "103 (0, [])\n",
      "104 (0, [])\n",
      "105 (0, [])\n",
      "106 (0, [])\n",
      "107 (0, [])\n",
      "108 (0, [])\n",
      "109 (0, [])\n",
      "110 (0, [])\n",
      "111 (0, [])\n",
      "112 (0, [])\n",
      "113 (0, [])\n",
      "114 (0, [])\n",
      "115 (0, [])\n",
      "116 (0, [])\n",
      "117 (0, [])\n",
      "118 (0, [])\n",
      "119 (0, [])\n",
      "120 (0, [])\n",
      "121 (0, [])\n",
      "122 (0, [])\n",
      "123 (0, [])\n",
      "124 (0, [])\n",
      "125 (0, [])\n",
      "126 (0, [])\n",
      "127 (0, [])\n",
      "128 (0, [])\n",
      "129 (0, [])\n",
      "130 (0, [])\n",
      "131 (0, [])\n",
      "132 (0, [])\n",
      "133 (0, [])\n",
      "134 (0, [])\n",
      "135 (0, [])\n",
      "136 (0, [])\n",
      "137 (0, [])\n",
      "138 (0, [])\n",
      "139 (0, [])\n",
      "140 (0, [])\n",
      "141 (0, [])\n",
      "142 (0, [])\n",
      "143 (0, [])\n",
      "144 (0, [])\n",
      "145 (0, [])\n",
      "146 (0, [])\n",
      "147 (0, [])\n",
      "148 (0, [])\n",
      "149 (0, [])\n",
      "150 (0, [])\n",
      "151 (0, [])\n",
      "152 (0, [])\n",
      "153 (0, [])\n",
      "154 (0, [])\n",
      "155 (0, [])\n",
      "156 (0, [])\n",
      "157 (0, [])\n",
      "158 (0, [])\n",
      "159 (0, [])\n",
      "160 (0, [])\n",
      "161 (0, [])\n",
      "162 (0, [])\n",
      "163 (0, [])\n",
      "164 (0, [])\n",
      "165 (0, [])\n",
      "166 (0, [])\n",
      "167 (0, [])\n",
      "168 (0, [])\n",
      "169 (0, [])\n",
      "170 (0, [])\n",
      "171 (0, [])\n",
      "172 (0, [])\n",
      "173 (0, [])\n",
      "174 (0, [])\n",
      "175 (0, [])\n",
      "176 (0, [])\n",
      "177 (0, [])\n",
      "178 (0, [])\n",
      "179 (0, [])\n",
      "180 (0, [])\n",
      "181 (0, [])\n",
      "182 (0, [])\n",
      "183 (0, [])\n",
      "184 (0, [])\n",
      "185 (0, [])\n",
      "186 (0, [])\n",
      "187 (0, [])\n",
      "188 (0, [])\n",
      "189 (0, [])\n",
      "190 (0, [])\n",
      "191 (0, [])\n",
      "192 (0, [])\n",
      "193 (0, [])\n",
      "194 (0, [])\n",
      "195 (0, [])\n",
      "196 (0, [])\n",
      "197 (0, [])\n",
      "198 (0, [])\n",
      "199 (0, [])\n",
      "200 (0, [])\n",
      "201 (0, [])\n",
      "202 (0, [])\n",
      "203 (0, [])\n",
      "204 (0, [])\n",
      "205 (0, [])\n",
      "206 (0, [])\n",
      "207 (0, [])\n",
      "208 (0, [])\n",
      "209 (0, [])\n",
      "210 (0, [])\n",
      "211 (0, [])\n",
      "212 (0, [])\n",
      "213 (0, [])\n",
      "214 (0, [])\n",
      "215 (0, [])\n",
      "216 (0, [])\n",
      "217 (0, [])\n",
      "218 (0, [])\n",
      "219 (0, [])\n",
      "220 (0, [])\n",
      "221 (0, [])\n",
      "222 (0, [])\n",
      "223 (0, [])\n",
      "224 (0, [])\n",
      "225 (0, [])\n",
      "226 (0, [])\n",
      "227 (0, [])\n",
      "228 (0, [])\n",
      "229 (0, [])\n",
      "230 (0, [])\n",
      "231 (0, [])\n",
      "232 (0, [])\n",
      "233 (0, [])\n",
      "234 (0, [])\n",
      "235 (0, [])\n",
      "236 (0, [])\n",
      "237 (0, [])\n",
      "238 (0, [])\n",
      "239 (0, [])\n",
      "240 (0, [])\n",
      "241 (0, [])\n",
      "242 (0, [])\n",
      "243 (0, [])\n",
      "244 (0, [])\n",
      "245 (0, [])\n",
      "246 (0, [])\n",
      "247 (0, [])\n",
      "248 (0, [])\n",
      "249 (0, [])\n",
      "250 (0, [])\n",
      "251 (0, [])\n",
      "252 (0, [])\n",
      "253 (0, [])\n",
      "254 (0, [])\n",
      "255 (0, [])\n"
     ]
    }
   ],
   "source": [
    "for i in range(256):\n",
    "    print(i, check_input(i))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "id": "broken-electric",
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.9.13"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 5
}
